package cz.cuni.mff.d3s.arcas.generator.alloy

import cz.cuni.mff.d3s.arcas.intermediate.*
import cz.cuni.mff.d3s.arcas.m2m.DRDLToIntermediate

import org.eclipse.emf.ecore.resource.Resource
import org.eclipse.emf.ecore.resource.ResourceSet
import org.eclipse.xtext.generator.extended.IGenerator2
import org.eclipse.xtext.generator.IFileSystemAccess
import static extension org.eclipse.xtext.xtend2.lib.ResourceExtensions.*

import com.google.common.collect.Iterables
import com.google.inject.Inject
import com.google.inject.internal.Lists

class DRDLGenerator implements IGenerator2 {

	@Inject extension GeneratorExtensions generatorExtensions

	/**
	 * Implementation note: This method is not used in IGenerator2, instead doGenerate() method for ResourceSet is used.
	 * The method is called (in addition to doGenerate() for ResourceSet), but we ignore it, because we are not able to
	 * generate the output from one resource only.
	 */
	override void doGenerate(Resource resource, IFileSystemAccess fsa) {
	}

	override void doGenerate(ResourceSet rs, IFileSystemAccess fsa) {
		println("Transformation to Alloy started.")
		val elements =
				rs.resources.map(r|r.allContentsIterable.filter(typeof(cz.cuni.mff.d3s.arcas.drdl.AbstractElement))).flatten
		var transformed = new DRDLToIntermediate().transform(elements)

		for (connector : transformed.connectors) {
			fsa.generateFile(connector.fileName, transformed.compile(connector))
			println("Generated " + connector.fileName + ".")
		}
	}

	def compile(IntermediateDocument doc, Connector connector) '''
		// ------------------------------------------------------------
		//  Meta-model
		// ------------------------------------------------------------

		«staticMetaModel()»

		// ------------------------------------------------------------
		//  Attributes (A)
		// ------------------------------------------------------------

		// TODO: duplicity
		«FOR ea : doc.elementArchitectures»
			«FOR feature : ea.features.filter(x|x.value != null)»
				«FOR attribute : feature.attributes»
					one sig «attribute.value.alloyNameA» extends Attribute {}
				«ENDFOR»
			«ENDFOR»
		«ENDFOR»

		// ------------------------------------------------------------
		//  Connector
		// ------------------------------------------------------------

		«connector(connector)»

		«staticConnectorPredicates()»

		// ------------------------------------------------------------
		//  Distribution Architecture (DA)
		// ------------------------------------------------------------

		«FOR da : doc.distributionArchitectures»
			«distributionArchitecture(da, doc.ports)»
		«ENDFOR»

		«staticDAPredicates()»

		// ------------------------------------------------------------
		//  DeploymentDocks (DD)
		// ------------------------------------------------------------

		«FOR dock : doc.docks»
			one sig «dock.alloyName» extends DeploymentDock {}
		«ENDFOR»

		// ------------------------------------------------------------
		//  Element Architectures (EA)
		// ------------------------------------------------------------

		«FOR ea : doc.elementArchitectures»
			one sig «ea.alloyName» extends ElementArchitecture {}
		«ENDFOR»

		«FOR ea : doc.elementArchitectures»
			«IF ea.subElements.isEmpty»
				«primitiveElementArchitecture(ea, doc.ports)»
			«ELSE»
				«compositeElementArchitecture(ea, doc.ports)»
			«ENDIF»
		«ENDFOR»

		«staticEAPredicates()»

		// ------------------------------------------------------------
		//  Endpoints (EP)
		// ------------------------------------------------------------

		«FOR c : doc.connectors»
			«FOR endpoint : c.endpoints»
				one sig «endpoint.alloyName» extends Endpoint {}
			«ENDFOR»
		«ENDFOR»

		// ------------------------------------------------------------
		//  Features (F, FV)
		// ------------------------------------------------------------

		«FOR featureName : doc.elementArchitectures.map(x|x.features).flatten.map(x|x.name).toSet»
			one sig «featureName.alloyNameF» extends Feature {}
		«ENDFOR»

		«FOR feature : doc.getUniqueFeatures»
			«featureValue(feature)»
		«ENDFOR»
		
		«FOR feature : connector.features.filter(x|x.component != null)»
			«FOR featureValue : feature.values»
				«featureValue(featureValue)»
			«ENDFOR»
		«ENDFOR»

		// ------------------------------------------------------------
		//  Ports (LPP, LRP, RP)
		// ------------------------------------------------------------

		«FOR port : doc.ports.filter(x|x.type == "LocalProvidedPort")»
			one sig «port.alloyName» extends LocalProvidedPort {}
		«ENDFOR»

		«FOR port : doc.ports.filter(x|x.type == "LocalRequiredPort")»
			one sig «port.alloyName» extends LocalRequiredPort {}
		«ENDFOR»

		«FOR port : doc.ports.filter(x|x.type == "RemotePort")»
			one sig «port.alloyName» extends RemotePort {}
		«ENDFOR»

		// ------------------------------------------------------------
		//  Roles (R)
		// ------------------------------------------------------------

		«FOR role : doc.roles»
			one sig «role.alloyName» extends Role {}
		«ENDFOR»

		// ------------------------------------------------------------
		//  Signatures (S)
		// ------------------------------------------------------------

		«FOR s : doc.signatures»
			«signature(s)»
		«ENDFOR»

		// ------------------------------------------------------------
		//  SubElementNames (SE)
		// ------------------------------------------------------------

		«FOR se : doc.subelements»
			one sig «se.alloyName» extends SubElementName {}
		«ENDFOR»

		// ------------------------------------------------------------
		//  UnitNames (U)
		// ------------------------------------------------------------

		«FOR da : doc.distributionArchitectures»
			«FOR unit : da.units»
				one sig «unit.alloyName» extends UnitName {}
			«ENDFOR»
		«ENDFOR»

		// ------------------------------------------------------------
		//  Run
		// ------------------------------------------------------------

		// TODO: for 8 ???
		run {} for 8
	'''

	def connector(Connector c) '''
		fact «c.alloyName» {
			DefinedEndpoints[«FOR endpoint : c.endpoints SEPARATOR " + "»«endpoint.alloyName»«ENDFOR»]
			AllowedDAs[«FOR da : c.allowedDAs SEPARATOR " + "»«da.alloyNameDa»«ENDFOR»]

			«FOR endpoint : c.endpoints»
				HasRole[«endpoint.alloyName», «endpoint.role.alloyNameRole»]
				HasSignature[«endpoint.alloyName», «endpoint.signature.alloyNameS»]
				IsDeployedOn[«endpoint.alloyName», «endpoint.dock.alloyNameDock»]

			«ENDFOR»

			-- definition of endpoints' features
			«FOR feature : c.features.filter(x|x.component != null)»
				EndpointFeatureRequirements[«feature.component.alloyNameEp(feature.interface)», «feature.alloyName», «feature.values.alloySetFv»]
			«ENDFOR»

			-- definition of global connectore features
			«FOR feature : c.features.filter(x|x.component == null)»
				ConnectorFeatureRequirements[«feature.alloyName», «feature.values.alloySetFv»]
			«ENDFOR»
		}
	'''

	def primitiveElementArchitecture(ElementArchitecture ea, Iterable<Port> ports) '''
		fact «ea.alloyName» {
			all e: Element | ElementHasEA[e, «ea.alloyName»] => {
				AllowedDeployment[e, «FOR dock: ea.allowedDeployments SEPARATOR " + "»«dock.alloyNameDock»«ENDFOR»]
				AvailablePorts[e, «FOR port: ea.availablePorts SEPARATOR " + "»«port.alloyNamePort(ports)»«ENDFOR»]
				SubElements[e, none]
				SupportedFeatures[e, «ea.features.alloySet»]
				RequiredAttributes[e, «ea.features.map(x|x.attributes.map(y|y.value)).flatten.alloySetA»]

				-- signature propagation
				«FOR sp : ea.signaturePropagations»
					«signaturePropagation(sp, ports)»
				«ENDFOR»

				-- enforcing values of the realized features
				«FOR f : ea.features»
					FeatureHasValue[e, «f.alloyName», «f.value.alloyNameFv»]
				«ENDFOR»

				-- defining attributes referred in feature values
				«FOR f : ea.features»
					«FOR a : f.attributes»
						FeatureValueUsesAttribute[e, «f.alloyName», «f.value.alloyNameFv»_«a.name», «a.value.alloyNameA»]
					«ENDFOR»
				«ENDFOR»
			}
		}

	'''

	def compositeElementArchitecture(ElementArchitecture ea, Iterable<Port> ports) '''
		fact «ea.alloyName» {
			all e: Element | ElementHasEA[e, «ea.alloyName»] => {
				AvailablePorts[e, «FOR port: ea.availablePorts SEPARATOR " + "»«port.alloyNamePort(ports)»«ENDFOR»]
				SubElements[e, «FOR se : ea.subElements SEPARATOR " + "»«se.alloyName»«ENDFOR»]
				SupportedFeatures[e, «FOR f : ea.features SEPARATOR " + "»«f.alloyName»«ENDFOR»]
				// XXX: Je toto potreba?
				//RequiredAttributes[e, Filename]

				-- definition of sub-elements
				«FOR se : ea.subElements»
					AllowedEAsForSubElement[e, «se.alloyName», «FOR ae : se.allowedEAs SEPARATOR " + "»«ae.alloyNameEa»«ENDFOR»]
					PropagateDeployment[e, «se.alloyName»]

				«ENDFOR»

				-- port bindings
				«FOR pb : ea.portBindings»
					«pb.portBinding(ports)»
				«ENDFOR»

				-- feature delegation
				«FOR f : ea.features»
					FeatureDelegation[e, «f.alloyName», «f.delegatedToSubElement.alloyNameSe», «f.delegatedToFeatureName.alloyNameF»]
				«ENDFOR»
			}
		}

	'''

	def signaturePropagation(ElementArchitectureSignaturePropagation sp, Iterable<Port> ports) '''
		«IF sp.destPortName != null»
			PropagateSignature[e, «sp.portName.alloyNamePort(ports)», «sp.destPortName.alloyNamePort(ports)»]
		«ELSE»
			PortHasSignature[e, «sp.portName.alloyNamePort(ports)», «sp.destSignature.alloyNameS»]
			«FOR a : sp.destSignatureAttributes»
				«IF !a.values.isEmpty»
					PortSignatureHasParameterValue[e, «sp.portName.alloyNamePort(ports)», «sp.destSignature.alloyNameS»_«a.name», «a.values.alloySetS»]
				«ELSE»
					PortSignatureHasParameterValue[e, «sp.portName.alloyNamePort(ports)», «sp.destSignature.alloyNameS»_«a.name», «FOR p : a.ports SEPARATOR " + "»e.ports[«p.alloyNamePort(ports)»]«ENDFOR»]
				«ENDIF»
			«ENDFOR»
		«ENDIF»
	'''

	def portBinding(ElementArchitecturePortBinding pb, Iterable<Port> ports) '''
		«IF pb.ffea1 == "this"»
			PortDelegation[e, «pb.eap1.alloyNamePort(ports)», «pb.ffea2.alloyNameSe», «pb.eap2.alloyNamePort(ports)»]
		«ELSEIF pb.ffea2 == "this"»
			PortDelegation[e, «pb.eap2.alloyNamePort(ports)», «pb.ffea1.alloyNameSe», «pb.eap1.alloyNamePort(ports)»]
		«ELSE»
			PortBinding[e, «pb.ffea1.alloyNameSe», «pb.eap1.alloyNamePort(ports)», «pb.ffea2.alloyNameSe», «pb.eap2.alloyNamePort(ports)»]
		«ENDIF»
	'''

	def distributionArchitecture(DistributionArchitecture da, Iterable<Port> ports) '''
		one sig «da.alloyName» extends DistributionArchitecture {}

		fact «da.alloyName» {
			EmployedDA[«da.alloyName»] => {
				AvailableRoles[«FOR role : da.roles SEPARATOR " + "»«role.alloyName»«ENDFOR»]
				RolesWithSingleCardinality[«FOR role : da.roles.filter(x|!x.multipleCardinality) SEPARATOR " + "»«role.alloyName»«ENDFOR»]
				RolesWithMultipleCardinality[«FOR role : da.roles.filter(x|x.multipleCardinality) SEPARATOR " + "»«role.alloyName»«ENDFOR»]

				AvailableUnits[«FOR unit : da.units SEPARATOR " + "»«unit.alloyName»«ENDFOR»]
				UnitsWithSingleCardinality[«FOR unit : da.units.filter(x|!x.multipleCardinality) SEPARATOR " + "»«unit.alloyName»«ENDFOR»]
				UnitsWithMultipleCardinality[«FOR unit : da.units.filter(x|x.multipleCardinality) SEPARATOR " + "»«unit.alloyName»«ENDFOR»]

				//SupportedFeatures[e, FT_Security]

				-- definition of units
				«FOR unit : da.units»
					AllowedEAsForUnit[«unit.alloyName», «FOR ea : unit.allowedEAs SEPARATOR " + "»«ea.alloyNameEa»«ENDFOR»]
					PortAssociatedWithRole[«unit.alloyName», «unit.associatedWithPort.alloyNamePort(ports)», «unit.associatedWithRole.alloyNameRole»]

				«ENDFOR»

				-- remote port bindings
				«FOR rb : da.remoteBindings»
					RemoteBinding[«rb.cau1.alloyNameUnit», «rb.eapr1.alloyNamePort(ports)», «rb.cau2.alloyNameUnit», «rb.eapr2.alloyNamePort(ports)»]
				«ENDFOR»

				-- feature delegation
				«FOR f : da.features»
					FeatureDelegation[«f.featureName.alloyNameF», «f.unit.alloyNameUnit», «f.unitFeatureName.alloyNameF»]
				«ENDFOR»
			}
		}

	'''

	def featureValue(ElementArchitectureFeature f) '''
		one sig «f.value.alloyNameFv» extends FeatureValue «f.featureAttributes()»
	'''
	
	def featureValue(ConnectorFeatureValue fv) '''
		one sig «fv.featureValueNameWithAttributes» extends «fv.name.alloyNameFv» {}
	'''
	
	def featureAttributes(ElementArchitectureFeature f) '''
		«IF f.attributes.empty»
			{}
		«ELSE»
			{
				«FOR fa : f.attributes SEPARATOR ","»
					«f.value.alloyNameFv»_«fa.name»: one AttributeValue
				«ENDFOR»
			}
		«ENDIF»
	'''

	def signature(Signature s) '''
		one sig «s.alloyName» extends Signature «s.signatureParameters()»
	'''

	def signatureParameters(Signature s) '''
		«IF s.parameters.empty»
			{}
		«ELSE»
			{
				«FOR sp : s.parameters SEPARATOR ","»
					«s.alloyName»_«sp»: one Signature
				«ENDFOR»
			}
		«ENDIF»
	'''

	// TODO: premiestnit staticke definicie do zvlastneho suboru

	def staticMetaModel() '''
		abstract sig Attribute {}
		abstract sig AttributeValue {}
		abstract sig DeploymentDock {}
		abstract sig DistributionArchitecture {}
		abstract sig ElementArchitecture {}
		abstract sig Endpoint {}
		abstract sig Feature {}
		abstract sig FeatureValue {}
		abstract sig LocalProvidedPort extends Port {}
		abstract sig LocalRequiredPort extends Port {}
		abstract sig Port {}
		abstract sig RemotePort extends Port {}
		abstract sig Role {}
		sig Signature {} // Signature is not abstract
		abstract sig SubElementName {}
		abstract sig UnitName {}

		abstract sig RoleInstance {
			signature: one Signature,
			role: one Role
		}

		abstract sig Element {
			elementArchitecture: one ElementArchitecture,
			ports: Port set -> lone Signature,
			subElements: SubElementName lone -> lone SubElement,
			dock: one DeploymentDock,
			features: Feature set -> lone FeatureValue,
			attributes: Attribute set -> lone AttributeValue
		}

		sig Unit extends Element {
			roleInstances: RoleInstance
		}

		sig SubElement extends Element {}

		one sig Connector {
			distributionArchitecture: one DistributionArchitecture,
			units: UnitName lone -> set Unit,
			connectorFeatures: Feature set -> lone FeatureValue
		}

		pred isSubElement[parent: Element, child: SubElement] {
			child in univ.(parent.subElements)
		}

		fact ElementHierarchyIsTree {
			-- There are no cycles among elements
			no iden & ^{ parent: Element, child: SubElement |
				isSubElement[parent, child] }

			-- Every element which is not a unit has exactly one owner
			all e: Element | e in Element - Unit <=>
				one owner: Element | isSubElement[owner, e]
		}
	'''

	def staticConnectorPredicates() '''
		pred DefinedEndpoints[ep: Endpoint] {
			// TODO
		}

		pred AllowedDAs[allowedDAs: set DistributionArchitecture] {
			// TODO
		}

		pred HasRole[ep: Endpoint, r: Role] {
			// TODO
		}

		pred HasSignature[ep: Endpoint, s: Signature] {
			// TODO
		}

		pred IsDeployedOn[ep: Endpoint, s: DeploymentDock] {
			// TODO
		}

		pred EndpointFeatureRequirements[ep: Endpoint, feature: Feature, values: set FeatureValue] {
			// TODO
		}

		pred ConnectorFeatureRequirements[feature: Feature, values: set FeatureValue] {
			// TODO
		}
	'''

	def staticDAPredicates() '''
		pred EmployedDA[da: DistributionArchitecture] {
			Connector.distributionArchitecture = da
		}

		pred AvailableRoles[roles: set Role] {
			Connector.units[univ].roleInstances.role = roles
		}

		pred RolesWithSingleCardinality[roles: set Role] {
			// TODO
		}

		pred RolesWithMultipleCardinality[roles: set Role] {
			// TODO
		}

		pred AvailableUnits[units: set UnitName] {
			// TODO
		}

		pred UnitsWithSingleCardinality[units: set UnitName] {
			// TODO
		}

		pred UnitsWithMultipleCardinality[units: set UnitName] {
			// TODO
		}

		pred AllowedEAsForUnit[unit: UnitName, allowedEAs: set ElementArchitecture] {
			// TODO
		}

		pred PortAssociatedWithRole[unit: UnitName, port: Port, role: Role] {
			// TODO
		}

		pred RemoteBinding[unit1: UnitName, p1: RemotePort,
		                   unit2: UnitName, p2: RemotePort]
		{
			Connector.units[unit1].ports[p1] = Connector.units[unit2].ports[p2]
		}

		pred FeatureDelegation[feature: Feature, unit: UnitName, unitFeature: Feature]
		{
			// TODO
		}
	'''

	def staticEAPredicates() '''
		pred ElementHasEA[e: Element, ea: ElementArchitecture] {
			e.elementArchitecture = ea
		}

		pred AllowedDeployment[e: Element, docks: set DeploymentDock] {
			// TODO
			e.dock in docks
		}

		pred AvailablePorts[e: Element, availablePorts: set Port] {
			e.ports.univ = availablePorts
		}

		pred SubElements[e: Element, elements: set SubElementName] {
			// TODO
			e.subElements.univ = elements
		}

		pred PortHasSignature[e: Element, port: Port, signature: Signature] {
			// TODO
		}

		pred PropagateSignature[e: Element, port1: Port, port2: Port] {
			// TODO
		}

		pred AllowedEAsForSubElement[e: Element, subelement: SubElementName, eas: set ElementArchitecture] {
			// TODO
		}

		pred PropagateDeployment[e: Element, subelement: SubElementName] {
			// TODO
		}

		pred PortBinding[e: Element,
		                 subelement1: SubElementName, port1: LocalRequiredPort,
		                 subelement2: SubElementName, port2: LocalProvidedPort]
		{
			e.subElements[subelement1].ports[port1] = e.subElements[subelement2].ports[port2]
		}

		pred PortDelegation[e: Element,
		                 port1: Port,
		                 subelement2: SubElementName, port2: Port]
		{
			// TODO
		}

		pred SupportedFeatures[e: Element, features: set Feature]
		{
			// TODO
		}

		pred RequiredAttributes[e: Element, attribute: Attribute]
		{
			// TODO
		}

		pred FeatureHasValue[e: Element, feature: Feature, value: FeatureValue]
		{
			// TODO
		}

		pred FeatureValueUsesAttribute[e: Element, feature: Feature, parameter: FeatureValue -> AttributeValue, attr: Attribute] {
			e.features[feature].parameter = e.attributes[attr]
		}

		pred FeatureDelegation[e: Element, feature: Feature, subelement: SubElementName, subelementFeature: Feature]
		{
			// TODO
		}

		pred PortSignatureHasParameterValue[e: Element, port: Port, parameter: Signature -> Signature, parameterValue: Signature]
		{
			e.ports[port].parameter = parameterValue
		}
	'''

}
